A, B:Realizer.
Rplus?(A)
 (i:Id. R-da(Rplus-left(A);i) || R-da(Rplus-right(A);i))
 (R-interface(A;B)  R-interface(Rplus-left(A);B) & R-interface(Rplus-right(A);B)) 

latex

Definitions

x:A. B(x), P  Q, b, Rplus?(x1), R-da(R;i), Rplus-left(x1), Rplus-right(x1), P  Q, R-interface(A;B), P & Q, Prop, t  T, x. t(x), false, true, if b t else f fi, P  Q, f(x)?z, Top, b, True, T, Realizer, Unit, x(s), False, , f || g, , , left  right, @loc x initially v:T, @loc only events in L change x:T, only events in L send on lnk with tag, @loc effect knd(v:T)  x := f State(ds) v , sends knd(v:T) on l:tagged(g,State(ds),v):dt, @loc precondition for a(v:T):P State(ds) v, @loc: k writes only members of L, @loc: k sends only on links in L, @loc: only members of L read x

Lemmas

unit wf, Id wf, Knd wf, IdLnk wf, fpf wf, decl-state wf, decl-type wf, false wf, es realizer wf, fpf-cap wf, fpf-join wf, fpf-join-cap-sq, Kind-deq wf, R-da wf, lsrc wf, fpf-trivial-subtype-top, top wf, rcv wf, fpf-dom wf, bool wf, eqtt to assert, btrue wf, ldst wf, fpf-ap wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, subtype rel wf, squash wf, true wf